Trait isotope::term::Substitute [−][src]
pub trait Substitute: Cons { type Substituted; fn subst_rec(
&self,
ctx: &mut impl SubstCtx + ?Sized
) -> Result<Option<Self::Substituted>, Error>; fn from_consed(
this: Self::Consed,
ctx: &mut impl ConsCtx + ?Sized
) -> Self::Substituted; fn shift(
&self,
shift: i32,
base: u32,
ctx: &mut impl ConsCtx + ?Sized
) -> Result<Option<Self::Substituted>, Error> { ... } fn shifted(
&self,
shift: i32,
base: u32,
ctx: &mut impl ConsCtx + ?Sized
) -> Result<Self::Substituted, Error> { ... } fn subst_vals<B>(
&self,
vals: &[B],
base: u32,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<Option<Self::Substituted>, Error>
where
B: Borrow<TermId>, { ... } }
Expand description
Objects which can be substituted in a context
Associated Types
type Substituted
[src]
type Substituted
[src]The type this substitutes to
Required methods
Substitute this value recursively
fn from_consed(
this: Self::Consed,
ctx: &mut impl ConsCtx + ?Sized
) -> Self::Substituted
[src]
fn from_consed(
this: Self::Consed,
ctx: &mut impl ConsCtx + ?Sized
) -> Self::Substituted
[src]Convert this object’s consed form to it’s substituted form
Provided methods
Shift this term’s variables with index >= base
in a given context
Shift this term’s variables with index >= base
in a given context